i:Id, T:Type{i}, s:T, R:(TT{i'}), poss:(ES{i}{i'}), ev:possible-event{i:l}(poss).
poss-consistent(i;T;s;ev;R)  {i'} 

latex

Definitions	Id, t  T, Type, , x:AB(x), ES, x:A. B(x), PossibleEvent(poss), pe-es(e), discrete state@i, pe-state(p), P & Q, f(a), pe-loc(p), s = t, x:A  B(x), A c B, poss-consistent(i;T;s;ev;R), {T}, P  Q, SQType(T), s ~ t, Atom$n
Lemmas	Id sq, pe-loc wf, es-dstate wf, pe-es wf, pe-state wf, possible-event wf, event system wf, Id wf